\begin{tabbing}
$\forall$\=$k$:Knd, $T$, $A$, $B$:Type, $l$:IdLnk, $x$, ${\it tg}$:Id, $f$:($A$$\rightarrow$$B$$\rightarrow$$T$), $c$:($A$$\rightarrow$$B$$\rightarrow\mathbb{B}$), ${\it es}$:ES.\+
\\[0ex]$k$(v:$B$) sends $f$($x$:$A$,v) on $l$ tagged with ${\it tg}$:$T$ provided $c$($x$,v) $\in$ $\mathbb{P}$
\-
\end{tabbing}